YES 1.6540000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| (((/=) :: Eq a => [a] -> [a] -> Bool) :: Eq a => [a] -> [a] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| (((/=) :: Eq a => [a] -> [a] -> Bool) :: Eq a => [a] -> [a] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| ((/=) :: Eq a => [a] -> [a] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2100), Succ(xv401000)) → new_primPlusNat(xv2100, xv401000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2100), Succ(xv401000)) → new_primPlusNat(xv2100, xv401000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(ty_[], bcc)) → new_esEs0(xv302, xv402, bcc)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_@2, baa), bab)), hf), hg)) → new_esEs1(xv300, xv400, baa, bab)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(app(ty_@2, bbc), bbd), hg) → new_esEs1(xv301, xv401, bbc, bbd)
new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(app(app(ty_@3, hb), hc), hd))) → new_esEs3(xv300, xv400, hb, hc, hd)
new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(app(ty_Either, gh), ha))) → new_esEs2(xv300, xv400, gh, ha)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, bac), bad), hf, hg) → new_esEs2(xv300, xv400, bac, bad)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(app(ty_Either, bbe), bbf)), hg)) → new_esEs2(xv301, xv401, bbe, bbf)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_[], hh)), hf), hg)) → new_esEs0(xv300, xv400, hh)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], ce), cd) → new_esEs0(xv300, xv400, ce)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, he), hf, hg) → new_esEs(xv300, xv400, he)
new_esEs(Just(xv300), Just(xv400), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xv300, xv400, bg, bh, ca)
new_esEs(Just(xv300), Just(xv400), app(app(ty_Either, be), bf)) → new_esEs2(xv300, xv400, be, bf)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(ty_Maybe, bcb))) → new_esEs(xv302, xv402, bcb)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(ty_[], bcc))) → new_esEs0(xv302, xv402, bcc)
new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(ty_Maybe, ba))) → new_esEs(xv300, xv400, ba)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(app(ty_@2, bcd), bce))) → new_esEs1(xv302, xv402, bcd, bce)
new_esEs(Just(xv300), Just(xv400), app(ty_Maybe, ba)) → new_esEs(xv300, xv400, ba)
new_esEs2(Left(xv300), Left(xv400), app(app(ty_Either, ff), fg), fa) → new_esEs2(xv300, xv400, ff, fg)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(ty_[], dh)) → new_esEs0(xv301, xv401, dh)
new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(ty_Maybe, gd))) → new_esEs(xv300, xv400, gd)
new_esEs2(Left(xv300), Left(xv400), app(app(app(ty_@3, fh), ga), gb), fa) → new_esEs3(xv300, xv400, fh, ga, gb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(ty_Maybe, bba), hg) → new_esEs(xv301, xv401, bba)
new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(ty_[], ge))) → new_esEs0(xv300, xv400, ge)
new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(app(ty_@3, bg), bh), ca))) → new_esEs3(xv300, xv400, bg, bh, ca)
new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(ty_@2, bc), bd))) → new_esEs1(xv300, xv400, bc, bd)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(ty_Maybe, dg))) → new_esEs(xv301, xv401, dg)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(app(ty_@2, ea), eb)) → new_esEs1(xv301, xv401, ea, eb)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(app(app(ty_@3, bch), bda), bdb))) → new_esEs3(xv302, xv402, bch, bda, bdb)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_Either, bac), bad)), hf), hg)) → new_esEs2(xv300, xv400, bac, bad)
new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(ty_@2, fc), fd)), fa)) → new_esEs1(xv300, xv400, fc, fd)
new_esEs2(Right(xv300), Right(xv400), gc, app(app(ty_Either, gh), ha)) → new_esEs2(xv300, xv400, gh, ha)
new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(ty_Either, be), bf))) → new_esEs2(xv300, xv400, be, bf)
new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(ty_Maybe, eh)), fa)) → new_esEs(xv300, xv400, eh)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(ty_@2, cf), cg)), cd)) → new_esEs1(xv300, xv400, cf, cg)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(app(ty_Either, ec), ed)) → new_esEs2(xv301, xv401, ec, ed)
new_esEs(Just(xv300), Just(xv400), app(app(ty_@2, bc), bd)) → new_esEs1(xv300, xv400, bc, bd)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(app(ty_@2, ea), eb))) → new_esEs1(xv301, xv401, ea, eb)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(ty_[], bbb)), hg)) → new_esEs0(xv301, xv401, bbb)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(ty_Maybe, dg)) → new_esEs(xv301, xv401, dg)
new_esEs2(Left(xv300), Left(xv400), app(ty_[], fb), fa) → new_esEs0(xv300, xv400, fb)
new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(app(ty_@2, gf), gg))) → new_esEs1(xv300, xv400, gf, gg)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(ty_Either, da), db)), cd)) → new_esEs2(xv300, xv400, da, db)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(ty_[], ce)), cd)) → new_esEs0(xv300, xv400, ce)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(app(ty_@3, bae), baf), bag)), hf), hg)) → new_esEs3(xv300, xv400, bae, baf, bag)
new_esEs2(Left(xv300), Left(xv400), app(app(ty_@2, fc), fd), fa) → new_esEs1(xv300, xv400, fc, fd)
new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(ty_[], fb)), fa)) → new_esEs0(xv300, xv400, fb)
new_esEs0(:(xv30, xv31), :(xv40, xv41), bdc) → new_esEs0(xv31, xv41, bdc)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(app(ty_@2, bbc), bbd)), hg)) → new_esEs1(xv301, xv401, bbc, bbd)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(ty_[], dh))) → new_esEs0(xv301, xv401, dh)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, da), db), cd) → new_esEs2(xv300, xv400, da, db)
new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(ty_[], bb))) → new_esEs0(xv300, xv400, bb)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xv301, xv401, ee, ef, eg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs3(xv302, xv402, bch, bda, bdb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(ty_[], bbb), hg) → new_esEs0(xv301, xv401, bbb)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xv301, xv401, ee, ef, eg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, baa), bab), hf, hg) → new_esEs1(xv300, xv400, baa, bab)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], hh), hf, hg) → new_esEs0(xv300, xv400, hh)
new_esEs2(Right(xv300), Right(xv400), gc, app(app(ty_@2, gf), gg)) → new_esEs1(xv300, xv400, gf, gg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(app(ty_Either, bbe), bbf), hg) → new_esEs2(xv301, xv401, bbe, bbf)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(app(ty_@3, dc), dd), de)), cd)) → new_esEs3(xv300, xv400, dc, dd, de)
new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(app(ty_@3, fh), ga), gb)), fa)) → new_esEs3(xv300, xv400, fh, ga, gb)
new_esEs(Just(xv300), Just(xv400), app(ty_[], bb)) → new_esEs0(xv300, xv400, bb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(ty_Maybe, bcb)) → new_esEs(xv302, xv402, bcb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(app(ty_Either, bcf), bcg)) → new_esEs2(xv302, xv402, bcf, bcg)
new_esEs2(Left(xv300), Left(xv400), app(ty_Maybe, eh), fa) → new_esEs(xv300, xv400, eh)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(app(app(ty_@3, bbg), bbh), bca), hg) → new_esEs3(xv301, xv401, bbg, bbh, bca)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(app(ty_@2, bcd), bce)) → new_esEs1(xv302, xv402, bcd, bce)
new_esEs2(Right(xv300), Right(xv400), gc, app(ty_Maybe, gd)) → new_esEs(xv300, xv400, gd)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(ty_Maybe, cc)), cd)) → new_esEs(xv300, xv400, cc)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xv300, xv400, dc, dd, de)
new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(ty_Either, ff), fg)), fa)) → new_esEs2(xv300, xv400, ff, fg)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, cf), cg), cd) → new_esEs1(xv300, xv400, cf, cg)
new_esEs2(Right(xv300), Right(xv400), gc, app(ty_[], ge)) → new_esEs0(xv300, xv400, ge)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(app(ty_Either, bcf), bcg))) → new_esEs2(xv302, xv402, bcf, bcg)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, cc), cd) → new_esEs(xv300, xv400, cc)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(app(ty_Either, ec), ed))) → new_esEs2(xv301, xv401, ec, ed)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(app(app(ty_@3, bbg), bbh), bca)), hg)) → new_esEs3(xv301, xv401, bbg, bbh, bca)
new_esEs0(:(xv30, xv31), :(xv40, xv41), app(ty_[], cb)) → new_esEs0(xv30, xv40, cb)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(ty_Maybe, bba)), hg)) → new_esEs(xv301, xv401, bba)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_Maybe, he)), hf), hg)) → new_esEs(xv300, xv400, he)
new_esEs2(Right(xv300), Right(xv400), gc, app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(xv300, xv400, hb, hc, hd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, bae), baf), bag), hf, hg) → new_esEs3(xv300, xv400, bae, baf, bag)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs(Just(xv300), Just(xv400), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xv300, xv400, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Just(xv300), Just(xv400), app(ty_[], bb)) → new_esEs0(xv300, xv400, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(xv300), Just(xv400), app(app(ty_@2, bc), bd)) → new_esEs1(xv300, xv400, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(xv300), Just(xv400), app(ty_Maybe, ba)) → new_esEs(xv300, xv400, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(xv300), Just(xv400), app(app(ty_Either, be), bf)) → new_esEs2(xv300, xv400, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(app(app(ty_@3, hb), hc), hd))) → new_esEs3(xv300, xv400, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(app(ty_@3, bg), bh), ca))) → new_esEs3(xv300, xv400, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(app(app(ty_@3, bch), bda), bdb))) → new_esEs3(xv302, xv402, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(app(ty_@3, bae), baf), bag)), hf), hg)) → new_esEs3(xv300, xv400, bae, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xv301, xv401, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(app(ty_@3, dc), dd), de)), cd)) → new_esEs3(xv300, xv400, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(app(ty_@3, fh), ga), gb)), fa)) → new_esEs3(xv300, xv400, fh, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(app(app(ty_@3, bbg), bbh), bca)), hg)) → new_esEs3(xv301, xv401, bbg, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_[], hh)), hf), hg)) → new_esEs0(xv300, xv400, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(ty_[], bcc))) → new_esEs0(xv302, xv402, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(ty_[], ge))) → new_esEs0(xv300, xv400, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(ty_[], bbb)), hg)) → new_esEs0(xv301, xv401, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(ty_[], ce)), cd)) → new_esEs0(xv300, xv400, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(ty_[], fb)), fa)) → new_esEs0(xv300, xv400, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xv30, xv31), :(xv40, xv41), bdc) → new_esEs0(xv31, xv41, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(ty_[], dh))) → new_esEs0(xv301, xv401, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(ty_[], bb))) → new_esEs0(xv300, xv400, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xv30, xv31), :(xv40, xv41), app(ty_[], cb)) → new_esEs0(xv30, xv40, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_@2, baa), bab)), hf), hg)) → new_esEs1(xv300, xv400, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(app(ty_@2, bcd), bce))) → new_esEs1(xv302, xv402, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(ty_@2, bc), bd))) → new_esEs1(xv300, xv400, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(ty_@2, fc), fd)), fa)) → new_esEs1(xv300, xv400, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(ty_@2, cf), cg)), cd)) → new_esEs1(xv300, xv400, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(app(ty_@2, ea), eb))) → new_esEs1(xv301, xv401, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(app(ty_@2, gf), gg))) → new_esEs1(xv300, xv400, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(app(ty_@2, bbc), bbd)), hg)) → new_esEs1(xv301, xv401, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(ty_Maybe, bcb))) → new_esEs(xv302, xv402, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(ty_Maybe, ba))) → new_esEs(xv300, xv400, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(ty_Maybe, gd))) → new_esEs(xv300, xv400, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(ty_Maybe, dg))) → new_esEs(xv301, xv401, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(ty_Maybe, eh)), fa)) → new_esEs(xv300, xv400, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(ty_Maybe, cc)), cd)) → new_esEs(xv300, xv400, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(ty_Maybe, bba)), hg)) → new_esEs(xv301, xv401, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_Maybe, he)), hf), hg)) → new_esEs(xv300, xv400, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, gc), app(app(ty_Either, gh), ha))) → new_esEs2(xv300, xv400, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), app(app(ty_Either, bbe), bbf)), hg)) → new_esEs2(xv301, xv401, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_Either, bac), bad)), hf), hg)) → new_esEs2(xv300, xv400, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(ty_Either, be), bf))) → new_esEs2(xv300, xv400, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(ty_Either, da), db)), cd)) → new_esEs2(xv300, xv400, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(ty_Either, ff), fg)), fa)) → new_esEs2(xv300, xv400, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, bah), hf), app(app(ty_Either, bcf), bcg))) → new_esEs2(xv302, xv402, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, df), app(app(ty_Either, ec), ed))) → new_esEs2(xv301, xv401, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xv301, xv401, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xv300, xv400, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs3(xv302, xv402, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(app(app(ty_@3, bbg), bbh), bca), hg) → new_esEs3(xv301, xv401, bbg, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, bae), baf), bag), hf, hg) → new_esEs3(xv300, xv400, bae, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(xv300), Left(xv400), app(app(app(ty_@3, fh), ga), gb), fa) → new_esEs3(xv300, xv400, fh, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xv300), Right(xv400), gc, app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(xv300, xv400, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], ce), cd) → new_esEs0(xv300, xv400, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(ty_[], dh)) → new_esEs0(xv301, xv401, dh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(app(ty_@2, ea), eb)) → new_esEs1(xv301, xv401, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, cf), cg), cd) → new_esEs1(xv300, xv400, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(ty_Maybe, dg)) → new_esEs(xv301, xv401, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, cc), cd) → new_esEs(xv300, xv400, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), df, app(app(ty_Either, ec), ed)) → new_esEs2(xv301, xv401, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, da), db), cd) → new_esEs2(xv300, xv400, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(ty_[], bcc)) → new_esEs0(xv302, xv402, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(ty_[], bbb), hg) → new_esEs0(xv301, xv401, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], hh), hf, hg) → new_esEs0(xv300, xv400, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(xv300), Left(xv400), app(ty_[], fb), fa) → new_esEs0(xv300, xv400, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv300), Right(xv400), gc, app(ty_[], ge)) → new_esEs0(xv300, xv400, ge)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(app(ty_@2, bbc), bbd), hg) → new_esEs1(xv301, xv401, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, baa), bab), hf, hg) → new_esEs1(xv300, xv400, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(app(ty_@2, bcd), bce)) → new_esEs1(xv302, xv402, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, he), hf, hg) → new_esEs(xv300, xv400, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(ty_Maybe, bba), hg) → new_esEs(xv301, xv401, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(ty_Maybe, bcb)) → new_esEs(xv302, xv402, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, bac), bad), hf, hg) → new_esEs2(xv300, xv400, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, app(app(ty_Either, bbe), bbf), hg) → new_esEs2(xv301, xv401, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), bah, hf, app(app(ty_Either, bcf), bcg)) → new_esEs2(xv302, xv402, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(Left(xv300), Left(xv400), app(app(ty_@2, fc), fd), fa) → new_esEs1(xv300, xv400, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv300), Right(xv400), gc, app(app(ty_@2, gf), gg)) → new_esEs1(xv300, xv400, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(xv300), Left(xv400), app(ty_Maybe, eh), fa) → new_esEs(xv300, xv400, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv300), Right(xv400), gc, app(ty_Maybe, gd)) → new_esEs(xv300, xv400, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xv300), Left(xv400), app(app(ty_Either, ff), fg), fa) → new_esEs2(xv300, xv400, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv300), Right(xv400), gc, app(app(ty_Either, gh), ha)) → new_esEs2(xv300, xv400, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4